Nuprl Definition : p-mu
11,40
postcript
pdf
p-mu(
P
;
x
)
== case
x
of inl(
n
) => (
(
P
(
n
))) & (
i
:{0..
n
}.
(
(
P
(
i
)))) | inr(
z
) =>
i
:
.
(
(
P
(
i
)))
latex
Definitions
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
P
&
Q
,
{
i
..
j
}
,
#$n
,
x
:
A
.
B
(
x
)
,
,
A
,
b
,
f
(
a
)
FDL editor aliases
p-mu
origin
(P(n))) & (
i:{0..n
}. 
((P(i)))) | inr(z) => i:
. ((P(i))) (P(n))) & (i:{0..n}. ((P(i)))) | inr(z) => i:. ((P(i))) }x:A. B(x)Ab